#+title: ats

#+date: <2018-05-22>

#+begin_quote
  ATS (Applied Type System) is a programming language designed to unify
  programming with formal specification. ATS has support for combining
  theorem proving with practical programming through the use of advanced
  type systems. A past version of The Computer Language Benchmarks Game
  has demonstrated that the performance of ATS is comparable to that of
  the C and C++ programming languages. By using theorem proving and
  strict type checking, the compiler can detect and prove that its
  implemented functions are not susceptible to bugs such as division by
  zero, memory leaks, buffer overflow, and other forms of memory
  corruption by verifying pointer arithmetic and reference counting
  before the program compiles. Additionally, by using the integrated
  theorem-proving system of ATS (ATS/LF), the programmer may make use of
  static constructs that are intertwined with the operative code to
  prove that a function attains its specification.
#+end_quote

[[https://en.wikipedia.org/wiki/ATS_(programming_language)][Wikipedia
entry on ATS]]
